The propositional Boolean satisfiability (SAT) problem is used in many applications, including software and hardware verification and computer aided design. Many advanced software analysis tools use SAT solving in their reasoning engines.
A propositional Boolean formula consists of Boolean variables connected by logical operators. Example operators include logical and (), logical or (), and logical negation (). Given such a formula, the SAT problem asks the question whether there exists a value assignment for the variables such that the formula evaluates to true under that assignment. The SAT problem is known to be NP-Complete. There exist many algorithms to solve SAT problems efficiently. As used herein, a propositional Boolean formula is simply referred to as a Boolean formula.
A quantified Boolean formula (QBF) is a more general form of Boolean formula that contains quantifiers. Example quantifiers include the universal quantifier ∀ and the existential quantifier ∃. The satisfiability problem for QBF is PSPACE-complete, which is considered to be computationally harder than NP-Complete. Conventional QBF algorithms do not perform well for many real-world applications. More effective QBF techniques are desirable.
One widely used approach to QBF solving is to transform the QBF formula into a quantifier-free Boolean formula that can be solved subsequently by a SAT solver. However, every time this kind of transformation is performed conventionally to eliminate the quantifier(s), a larger formula results, which is undesirable.
In view of the foregoing, there is a need for systems and methods that overcome such deficiencies.